(0) Obligation:
Clauses:
overlap(Xs, Ys) :- ','(member2(X, Xs), member1(X, Ys)).
has_a_or_b(Xs) :- overlap(Xs, .(a, .(b, []))).
member1(X, .(Y, Xs)) :- member1(X, Xs).
member1(X, .(X, Xs)).
member2(X, .(Y, Xs)) :- member2(X, Xs).
member2(X, .(X, Xs)).
Query: overlap(g,g)
(1) PrologToPrologProblemTransformerProof (SOUND transformation)
Built Prolog problem from termination graph ICLP10.
(2) Obligation:
Clauses:
pA(X25, .(T15, T16), T6) :- pA(X25, T16, T6).
pA(T23, .(T23, T24), T6) :- member1B(T23, T6).
member1B(T40, .(T41, T42)) :- member1B(T40, T42).
member1B(T50, .(T50, T51)).
overlapC(T5, T6) :- pA(X5, T5, T6).
Query: overlapC(g,g)
(3) PrologToPiTRSProof (SOUND transformation)
We use the technique of [TOCL09]. With regard to the inferred argument filtering the predicates were used in the following modes:
overlapC_in: (b,b)
pA_in: (f,b,b)
member1B_in: (b,b)
Transforming
Prolog into the following
Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
overlapC_in_gg(T5, T6) → U4_gg(T5, T6, pA_in_agg(X5, T5, T6))
pA_in_agg(X25, .(T15, T16), T6) → U1_agg(X25, T15, T16, T6, pA_in_agg(X25, T16, T6))
pA_in_agg(T23, .(T23, T24), T6) → U2_agg(T23, T24, T6, member1B_in_gg(T23, T6))
member1B_in_gg(T40, .(T41, T42)) → U3_gg(T40, T41, T42, member1B_in_gg(T40, T42))
member1B_in_gg(T50, .(T50, T51)) → member1B_out_gg(T50, .(T50, T51))
U3_gg(T40, T41, T42, member1B_out_gg(T40, T42)) → member1B_out_gg(T40, .(T41, T42))
U2_agg(T23, T24, T6, member1B_out_gg(T23, T6)) → pA_out_agg(T23, .(T23, T24), T6)
U1_agg(X25, T15, T16, T6, pA_out_agg(X25, T16, T6)) → pA_out_agg(X25, .(T15, T16), T6)
U4_gg(T5, T6, pA_out_agg(X5, T5, T6)) → overlapC_out_gg(T5, T6)
The argument filtering Pi contains the following mapping:
overlapC_in_gg(
x1,
x2) =
overlapC_in_gg(
x1,
x2)
U4_gg(
x1,
x2,
x3) =
U4_gg(
x3)
pA_in_agg(
x1,
x2,
x3) =
pA_in_agg(
x2,
x3)
.(
x1,
x2) =
.(
x1,
x2)
U1_agg(
x1,
x2,
x3,
x4,
x5) =
U1_agg(
x5)
U2_agg(
x1,
x2,
x3,
x4) =
U2_agg(
x1,
x4)
member1B_in_gg(
x1,
x2) =
member1B_in_gg(
x1,
x2)
U3_gg(
x1,
x2,
x3,
x4) =
U3_gg(
x4)
member1B_out_gg(
x1,
x2) =
member1B_out_gg
pA_out_agg(
x1,
x2,
x3) =
pA_out_agg(
x1)
overlapC_out_gg(
x1,
x2) =
overlapC_out_gg
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
(4) Obligation:
Pi-finite rewrite system:
The TRS R consists of the following rules:
overlapC_in_gg(T5, T6) → U4_gg(T5, T6, pA_in_agg(X5, T5, T6))
pA_in_agg(X25, .(T15, T16), T6) → U1_agg(X25, T15, T16, T6, pA_in_agg(X25, T16, T6))
pA_in_agg(T23, .(T23, T24), T6) → U2_agg(T23, T24, T6, member1B_in_gg(T23, T6))
member1B_in_gg(T40, .(T41, T42)) → U3_gg(T40, T41, T42, member1B_in_gg(T40, T42))
member1B_in_gg(T50, .(T50, T51)) → member1B_out_gg(T50, .(T50, T51))
U3_gg(T40, T41, T42, member1B_out_gg(T40, T42)) → member1B_out_gg(T40, .(T41, T42))
U2_agg(T23, T24, T6, member1B_out_gg(T23, T6)) → pA_out_agg(T23, .(T23, T24), T6)
U1_agg(X25, T15, T16, T6, pA_out_agg(X25, T16, T6)) → pA_out_agg(X25, .(T15, T16), T6)
U4_gg(T5, T6, pA_out_agg(X5, T5, T6)) → overlapC_out_gg(T5, T6)
The argument filtering Pi contains the following mapping:
overlapC_in_gg(
x1,
x2) =
overlapC_in_gg(
x1,
x2)
U4_gg(
x1,
x2,
x3) =
U4_gg(
x3)
pA_in_agg(
x1,
x2,
x3) =
pA_in_agg(
x2,
x3)
.(
x1,
x2) =
.(
x1,
x2)
U1_agg(
x1,
x2,
x3,
x4,
x5) =
U1_agg(
x5)
U2_agg(
x1,
x2,
x3,
x4) =
U2_agg(
x1,
x4)
member1B_in_gg(
x1,
x2) =
member1B_in_gg(
x1,
x2)
U3_gg(
x1,
x2,
x3,
x4) =
U3_gg(
x4)
member1B_out_gg(
x1,
x2) =
member1B_out_gg
pA_out_agg(
x1,
x2,
x3) =
pA_out_agg(
x1)
overlapC_out_gg(
x1,
x2) =
overlapC_out_gg
(5) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:
OVERLAPC_IN_GG(T5, T6) → U4_GG(T5, T6, pA_in_agg(X5, T5, T6))
OVERLAPC_IN_GG(T5, T6) → PA_IN_AGG(X5, T5, T6)
PA_IN_AGG(X25, .(T15, T16), T6) → U1_AGG(X25, T15, T16, T6, pA_in_agg(X25, T16, T6))
PA_IN_AGG(X25, .(T15, T16), T6) → PA_IN_AGG(X25, T16, T6)
PA_IN_AGG(T23, .(T23, T24), T6) → U2_AGG(T23, T24, T6, member1B_in_gg(T23, T6))
PA_IN_AGG(T23, .(T23, T24), T6) → MEMBER1B_IN_GG(T23, T6)
MEMBER1B_IN_GG(T40, .(T41, T42)) → U3_GG(T40, T41, T42, member1B_in_gg(T40, T42))
MEMBER1B_IN_GG(T40, .(T41, T42)) → MEMBER1B_IN_GG(T40, T42)
The TRS R consists of the following rules:
overlapC_in_gg(T5, T6) → U4_gg(T5, T6, pA_in_agg(X5, T5, T6))
pA_in_agg(X25, .(T15, T16), T6) → U1_agg(X25, T15, T16, T6, pA_in_agg(X25, T16, T6))
pA_in_agg(T23, .(T23, T24), T6) → U2_agg(T23, T24, T6, member1B_in_gg(T23, T6))
member1B_in_gg(T40, .(T41, T42)) → U3_gg(T40, T41, T42, member1B_in_gg(T40, T42))
member1B_in_gg(T50, .(T50, T51)) → member1B_out_gg(T50, .(T50, T51))
U3_gg(T40, T41, T42, member1B_out_gg(T40, T42)) → member1B_out_gg(T40, .(T41, T42))
U2_agg(T23, T24, T6, member1B_out_gg(T23, T6)) → pA_out_agg(T23, .(T23, T24), T6)
U1_agg(X25, T15, T16, T6, pA_out_agg(X25, T16, T6)) → pA_out_agg(X25, .(T15, T16), T6)
U4_gg(T5, T6, pA_out_agg(X5, T5, T6)) → overlapC_out_gg(T5, T6)
The argument filtering Pi contains the following mapping:
overlapC_in_gg(
x1,
x2) =
overlapC_in_gg(
x1,
x2)
U4_gg(
x1,
x2,
x3) =
U4_gg(
x3)
pA_in_agg(
x1,
x2,
x3) =
pA_in_agg(
x2,
x3)
.(
x1,
x2) =
.(
x1,
x2)
U1_agg(
x1,
x2,
x3,
x4,
x5) =
U1_agg(
x5)
U2_agg(
x1,
x2,
x3,
x4) =
U2_agg(
x1,
x4)
member1B_in_gg(
x1,
x2) =
member1B_in_gg(
x1,
x2)
U3_gg(
x1,
x2,
x3,
x4) =
U3_gg(
x4)
member1B_out_gg(
x1,
x2) =
member1B_out_gg
pA_out_agg(
x1,
x2,
x3) =
pA_out_agg(
x1)
overlapC_out_gg(
x1,
x2) =
overlapC_out_gg
OVERLAPC_IN_GG(
x1,
x2) =
OVERLAPC_IN_GG(
x1,
x2)
U4_GG(
x1,
x2,
x3) =
U4_GG(
x3)
PA_IN_AGG(
x1,
x2,
x3) =
PA_IN_AGG(
x2,
x3)
U1_AGG(
x1,
x2,
x3,
x4,
x5) =
U1_AGG(
x5)
U2_AGG(
x1,
x2,
x3,
x4) =
U2_AGG(
x1,
x4)
MEMBER1B_IN_GG(
x1,
x2) =
MEMBER1B_IN_GG(
x1,
x2)
U3_GG(
x1,
x2,
x3,
x4) =
U3_GG(
x4)
We have to consider all (P,R,Pi)-chains
(6) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
OVERLAPC_IN_GG(T5, T6) → U4_GG(T5, T6, pA_in_agg(X5, T5, T6))
OVERLAPC_IN_GG(T5, T6) → PA_IN_AGG(X5, T5, T6)
PA_IN_AGG(X25, .(T15, T16), T6) → U1_AGG(X25, T15, T16, T6, pA_in_agg(X25, T16, T6))
PA_IN_AGG(X25, .(T15, T16), T6) → PA_IN_AGG(X25, T16, T6)
PA_IN_AGG(T23, .(T23, T24), T6) → U2_AGG(T23, T24, T6, member1B_in_gg(T23, T6))
PA_IN_AGG(T23, .(T23, T24), T6) → MEMBER1B_IN_GG(T23, T6)
MEMBER1B_IN_GG(T40, .(T41, T42)) → U3_GG(T40, T41, T42, member1B_in_gg(T40, T42))
MEMBER1B_IN_GG(T40, .(T41, T42)) → MEMBER1B_IN_GG(T40, T42)
The TRS R consists of the following rules:
overlapC_in_gg(T5, T6) → U4_gg(T5, T6, pA_in_agg(X5, T5, T6))
pA_in_agg(X25, .(T15, T16), T6) → U1_agg(X25, T15, T16, T6, pA_in_agg(X25, T16, T6))
pA_in_agg(T23, .(T23, T24), T6) → U2_agg(T23, T24, T6, member1B_in_gg(T23, T6))
member1B_in_gg(T40, .(T41, T42)) → U3_gg(T40, T41, T42, member1B_in_gg(T40, T42))
member1B_in_gg(T50, .(T50, T51)) → member1B_out_gg(T50, .(T50, T51))
U3_gg(T40, T41, T42, member1B_out_gg(T40, T42)) → member1B_out_gg(T40, .(T41, T42))
U2_agg(T23, T24, T6, member1B_out_gg(T23, T6)) → pA_out_agg(T23, .(T23, T24), T6)
U1_agg(X25, T15, T16, T6, pA_out_agg(X25, T16, T6)) → pA_out_agg(X25, .(T15, T16), T6)
U4_gg(T5, T6, pA_out_agg(X5, T5, T6)) → overlapC_out_gg(T5, T6)
The argument filtering Pi contains the following mapping:
overlapC_in_gg(
x1,
x2) =
overlapC_in_gg(
x1,
x2)
U4_gg(
x1,
x2,
x3) =
U4_gg(
x3)
pA_in_agg(
x1,
x2,
x3) =
pA_in_agg(
x2,
x3)
.(
x1,
x2) =
.(
x1,
x2)
U1_agg(
x1,
x2,
x3,
x4,
x5) =
U1_agg(
x5)
U2_agg(
x1,
x2,
x3,
x4) =
U2_agg(
x1,
x4)
member1B_in_gg(
x1,
x2) =
member1B_in_gg(
x1,
x2)
U3_gg(
x1,
x2,
x3,
x4) =
U3_gg(
x4)
member1B_out_gg(
x1,
x2) =
member1B_out_gg
pA_out_agg(
x1,
x2,
x3) =
pA_out_agg(
x1)
overlapC_out_gg(
x1,
x2) =
overlapC_out_gg
OVERLAPC_IN_GG(
x1,
x2) =
OVERLAPC_IN_GG(
x1,
x2)
U4_GG(
x1,
x2,
x3) =
U4_GG(
x3)
PA_IN_AGG(
x1,
x2,
x3) =
PA_IN_AGG(
x2,
x3)
U1_AGG(
x1,
x2,
x3,
x4,
x5) =
U1_AGG(
x5)
U2_AGG(
x1,
x2,
x3,
x4) =
U2_AGG(
x1,
x4)
MEMBER1B_IN_GG(
x1,
x2) =
MEMBER1B_IN_GG(
x1,
x2)
U3_GG(
x1,
x2,
x3,
x4) =
U3_GG(
x4)
We have to consider all (P,R,Pi)-chains
(7) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 6 less nodes.
(8) Complex Obligation (AND)
(9) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
MEMBER1B_IN_GG(T40, .(T41, T42)) → MEMBER1B_IN_GG(T40, T42)
The TRS R consists of the following rules:
overlapC_in_gg(T5, T6) → U4_gg(T5, T6, pA_in_agg(X5, T5, T6))
pA_in_agg(X25, .(T15, T16), T6) → U1_agg(X25, T15, T16, T6, pA_in_agg(X25, T16, T6))
pA_in_agg(T23, .(T23, T24), T6) → U2_agg(T23, T24, T6, member1B_in_gg(T23, T6))
member1B_in_gg(T40, .(T41, T42)) → U3_gg(T40, T41, T42, member1B_in_gg(T40, T42))
member1B_in_gg(T50, .(T50, T51)) → member1B_out_gg(T50, .(T50, T51))
U3_gg(T40, T41, T42, member1B_out_gg(T40, T42)) → member1B_out_gg(T40, .(T41, T42))
U2_agg(T23, T24, T6, member1B_out_gg(T23, T6)) → pA_out_agg(T23, .(T23, T24), T6)
U1_agg(X25, T15, T16, T6, pA_out_agg(X25, T16, T6)) → pA_out_agg(X25, .(T15, T16), T6)
U4_gg(T5, T6, pA_out_agg(X5, T5, T6)) → overlapC_out_gg(T5, T6)
The argument filtering Pi contains the following mapping:
overlapC_in_gg(
x1,
x2) =
overlapC_in_gg(
x1,
x2)
U4_gg(
x1,
x2,
x3) =
U4_gg(
x3)
pA_in_agg(
x1,
x2,
x3) =
pA_in_agg(
x2,
x3)
.(
x1,
x2) =
.(
x1,
x2)
U1_agg(
x1,
x2,
x3,
x4,
x5) =
U1_agg(
x5)
U2_agg(
x1,
x2,
x3,
x4) =
U2_agg(
x1,
x4)
member1B_in_gg(
x1,
x2) =
member1B_in_gg(
x1,
x2)
U3_gg(
x1,
x2,
x3,
x4) =
U3_gg(
x4)
member1B_out_gg(
x1,
x2) =
member1B_out_gg
pA_out_agg(
x1,
x2,
x3) =
pA_out_agg(
x1)
overlapC_out_gg(
x1,
x2) =
overlapC_out_gg
MEMBER1B_IN_GG(
x1,
x2) =
MEMBER1B_IN_GG(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(10) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(11) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
MEMBER1B_IN_GG(T40, .(T41, T42)) → MEMBER1B_IN_GG(T40, T42)
R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
(12) PiDPToQDPProof (EQUIVALENT transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(13) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MEMBER1B_IN_GG(T40, .(T41, T42)) → MEMBER1B_IN_GG(T40, T42)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(14) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- MEMBER1B_IN_GG(T40, .(T41, T42)) → MEMBER1B_IN_GG(T40, T42)
The graph contains the following edges 1 >= 1, 2 > 2
(15) YES
(16) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
PA_IN_AGG(X25, .(T15, T16), T6) → PA_IN_AGG(X25, T16, T6)
The TRS R consists of the following rules:
overlapC_in_gg(T5, T6) → U4_gg(T5, T6, pA_in_agg(X5, T5, T6))
pA_in_agg(X25, .(T15, T16), T6) → U1_agg(X25, T15, T16, T6, pA_in_agg(X25, T16, T6))
pA_in_agg(T23, .(T23, T24), T6) → U2_agg(T23, T24, T6, member1B_in_gg(T23, T6))
member1B_in_gg(T40, .(T41, T42)) → U3_gg(T40, T41, T42, member1B_in_gg(T40, T42))
member1B_in_gg(T50, .(T50, T51)) → member1B_out_gg(T50, .(T50, T51))
U3_gg(T40, T41, T42, member1B_out_gg(T40, T42)) → member1B_out_gg(T40, .(T41, T42))
U2_agg(T23, T24, T6, member1B_out_gg(T23, T6)) → pA_out_agg(T23, .(T23, T24), T6)
U1_agg(X25, T15, T16, T6, pA_out_agg(X25, T16, T6)) → pA_out_agg(X25, .(T15, T16), T6)
U4_gg(T5, T6, pA_out_agg(X5, T5, T6)) → overlapC_out_gg(T5, T6)
The argument filtering Pi contains the following mapping:
overlapC_in_gg(
x1,
x2) =
overlapC_in_gg(
x1,
x2)
U4_gg(
x1,
x2,
x3) =
U4_gg(
x3)
pA_in_agg(
x1,
x2,
x3) =
pA_in_agg(
x2,
x3)
.(
x1,
x2) =
.(
x1,
x2)
U1_agg(
x1,
x2,
x3,
x4,
x5) =
U1_agg(
x5)
U2_agg(
x1,
x2,
x3,
x4) =
U2_agg(
x1,
x4)
member1B_in_gg(
x1,
x2) =
member1B_in_gg(
x1,
x2)
U3_gg(
x1,
x2,
x3,
x4) =
U3_gg(
x4)
member1B_out_gg(
x1,
x2) =
member1B_out_gg
pA_out_agg(
x1,
x2,
x3) =
pA_out_agg(
x1)
overlapC_out_gg(
x1,
x2) =
overlapC_out_gg
PA_IN_AGG(
x1,
x2,
x3) =
PA_IN_AGG(
x2,
x3)
We have to consider all (P,R,Pi)-chains
(17) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(18) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
PA_IN_AGG(X25, .(T15, T16), T6) → PA_IN_AGG(X25, T16, T6)
R is empty.
The argument filtering Pi contains the following mapping:
.(
x1,
x2) =
.(
x1,
x2)
PA_IN_AGG(
x1,
x2,
x3) =
PA_IN_AGG(
x2,
x3)
We have to consider all (P,R,Pi)-chains
(19) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(20) Obligation:
Q DP problem:
The TRS P consists of the following rules:
PA_IN_AGG(.(T15, T16), T6) → PA_IN_AGG(T16, T6)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(21) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- PA_IN_AGG(.(T15, T16), T6) → PA_IN_AGG(T16, T6)
The graph contains the following edges 1 > 1, 2 >= 2
(22) YES